es:ES, e:E, i:Id. loc-on-path(es;i;[e])  (loc(e) = i) 

latex

Definitions	s = t, t  T, ES, E, Id, x:A  B(x), b, let x,y = A in B(x;y), t.1, Atom$n, False, loc(e), Type, , P  Q, left + right, , x:AB(x), P  Q, P  Q, locl(a), Knd, x:A. B(x), (x  l), P & Q, P  Q, loc-on-path(es;i;L)
Lemmas	event system wf, es-E wf, loc-on-path-cons, iff functionality wrt iff, loc-on-path wf, or functionality wrt iff, loc-on-path-nil, iff wf, rev implies wf, Id wf, false wf